es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Try(e1)  (j  L)  ((j = loc(e1)))  (isrcv(the rcv(wanted message from e1 to j)))) 

latex

Definitions	, True, if b then t else f fi , tt, t  T, IdLnk, "$x", the rcv(wanted message from e1 to j), isrcv(e), b, P  Q, Id, x:A. B(x), xL. P(x), P & Q, A c B, Try(e), fischer(L)
Lemmas	event system wf, fischer wf, es-E wf, f-try wf, l member wf, es-loc wf, Id wf, not wf, es-kind-first-from